#include "mainwindow.h"
#include "ui_mainwindow.h"
#include "ruledialog.h"
#include "ruleitemwidget.h"


MainWindow::MainWindow(QWidget *parent) :
    QMainWindow(parent),
    ui(new Ui::MainWindow)
{
    mNumVariable = 0;
    ui->setupUi(this);
    ui->mVariableTableWidget->horizontalHeader()->setResizeMode(QHeaderView::ResizeToContents);
    ui->mPathTableWidget->horizontalHeader()->setResizeMode(QHeaderView::ResizeToContents);
    ui->mStackedLeftWidget->setCurrentIndex(0);
    mIsMannual = false;
}

MainWindow::~MainWindow()
{
    delete ui;
}

void MainWindow::on_mNumVariableSpin_valueChanged(int arg1)
{
    if (arg1 < 0) {
        return;
    }

    if (arg1 > mNumVariable) {
        ui->mVariableTableWidget->insertRow(ui->mVariableTableWidget->rowCount());
        ui->mVariableTableWidget->insertColumn(ui->mVariableTableWidget->columnCount());

        ui->mPathTableWidget->insertRow(ui->mPathTableWidget->rowCount());
        ui->mPathTableWidget->insertColumn(ui->mPathTableWidget->columnCount());

        mNumVariable = arg1;
    }

    if (arg1 < mNumVariable) {
        ui->mVariableTableWidget->removeRow(ui->mVariableTableWidget->rowCount() - 1);
        ui->mVariableTableWidget->removeColumn(ui->mVariableTableWidget->columnCount() - 1);

        ui->mPathTableWidget->removeRow(ui->mPathTableWidget->rowCount() - 1);
        ui->mPathTableWidget->removeColumn(ui->mPathTableWidget->columnCount() - 1);

        mNumVariable = arg1;
    }
}

void MainWindow::on_mClearOutputButton_clicked()
{
    ui->mOutputTextEdit->clear();
}

void MainWindow::on_mProveSequentButton_clicked()
{

    //Create sequent to prove
    std::string sequent_string;
    sequent_string = ui->mInputSequentEdit->text().toUtf8().constData();

    if (sequent_string.length() <= 0) {
        QMessageBox *box = new QMessageBox(this);
        box->setText(QString("Input sequent is empty!"));
        box->show();
        return;
    }

    Sequent *input = new Sequent(sequent_string);


    if (!mIsMannual) {
        //Create agent
        Agent *agent = new Agent("A");

        //Create all atomic propositional variables
        std::vector<AtomicProposition*> atomicPropositionList;
        for (size_t i = 0; i < mNumVariable; i++) {
            std::string str("ap{p_{");
            std::stringstream num;
            num << i+1;
            str += num.str();
            str += "}}";
            atomicPropositionList.push_back(new AtomicProposition(str));
        }

        //Create map matrix from table
        std::vector<std::string> matrix = generateMatrix(ui->mVariableTableWidget);

        //Create action list
        std::vector<AtomicAction*> actionList = generateActionList(matrix);

        //Create action appearance rules
        std::vector<R_App*> actionAppRuleList;
        for (size_t i = 0; i < actionList.size(); i++) {
            actionAppRuleList.push_back(new R_App(agent, actionList[i], actionList[i]));
        }

        //Create propositional variable appearance rules
        std::vector<R_PrApp*>   variablePrAppRuleList;
        for (size_t i = 0; i < mNumVariable; i++) {
            Proposition *p = atomicPropositionList.at(i);
            std::vector<AtomicProposition*> uncertain = getUncertainVariables(i, atomicPropositionList, matrix);
            Proposition *q = getNestedDisjunction(uncertain);
            variablePrAppRuleList.push_back(new R_PrApp(agent, p, q));
        }

        //Create navigation appearance rules
        std::vector<NavApp*> navAppRules;
        for (int row = 0; row < mNumVariable; row++) {
            for (int action = 0; action < actionList.size(); action++) {
                std::vector<AtomicProposition*> destinations;

                for (int column = 0; column < mNumVariable; column++) {
                    if (matrix.at(row * mNumVariable + column).compare(actionList.at(action)->toString()) == 0) {
                        destinations.push_back(atomicPropositionList.at(column));
                    }
                }

                if (destinations.size() <= 0) {
                    std::string b ("bt");
                    Bottom *bottom = new Bottom(b);
                    navAppRules.push_back(new NavApp(atomicPropositionList.at(row), actionList.at(action), bottom));
                } else {
                    Proposition* p = getNestedDisjunction(destinations);
                    navAppRules.push_back(new NavApp(atomicPropositionList.at(row), actionList.at(action), p));
                }
            }
        }

        //Create real path
        NavPath *navpath = new NavPath();
        getPath(navpath, atomicPropositionList, matrix );

        NavFNDyDist *navfndydist = new NavFNDyDist(navpath);

        std::vector<Rule*> ruleList;

        ruleList.push_back(navfndydist);

        for (size_t i = 0; i < variablePrAppRuleList.size(); i++) {
            ruleList.push_back(variablePrAppRuleList.at(i));
        }

        for (size_t i = 0; i < actionAppRuleList.size(); i++) {
            ruleList.push_back(actionAppRuleList.at(i));
        }

        for (size_t i = 0; i < navAppRules.size(); i++) {
            ruleList.push_back(navAppRules.at(i));
        }

        std::vector<Rule*> sysRule = registerAllRules();

        for(size_t i = 0; i < sysRule.size(); i++) {
            ruleList.push_back(sysRule.at(i));
        }

        Configuration conf(input, &ruleList);

        if (conf.prove()) {
            //std::cout << conf.toLatex() << std::endl;
            mResult = conf.toLatex();
            QString string = QString::fromStdString(mResult);
            QTextCursor cursor(ui->mOutputTextEdit->document());
            cursor.insertText(string);
        }
    } else {
        Configuration conf(input, &mRuleList);

        if (conf.prove()) {
            //std::cout << conf.toLatex() << std::endl;
            mResult = conf.toLatex();
            QString string = QString::fromStdString(mResult);
            QTextCursor cursor(ui->mOutputTextEdit->document());
            cursor.insertText(string);
        }
    }
}

void MainWindow::getPath(NavPath *path, std::vector<AtomicProposition *> variableList, std::vector<std::string> matrix) {
    for (int row = 0; row < mNumVariable; row++) {
        for (int column = 0; column< mNumVariable; column++) {
            if (ui->mPathTableWidget->item(row, column) != 0) {
                int current = row;
                int next_hop = column;
                std::string action = matrix.at(current * mNumVariable + next_hop);
                while (next_hop >= 0) {
                    path->add(new NavStep(variableList.at(current), new AtomicAction(action), variableList.at(next_hop)));
                    std::cout << "Add path:" << variableList.at(current)->toString() << "," << variableList.at(next_hop)->toString() << std::endl;
                    current = next_hop;
                    next_hop = -1;
                    for (int s = 0; s < mNumVariable; s++) {
                        if (ui->mPathTableWidget->item(current, s) != 0) {
                            next_hop = s;
                            action = matrix.at(current * mNumVariable + next_hop);
                            break;
                        }
                    }
                }
                return;
            }
        }
    }
}

Proposition* MainWindow::getNestedDisjunction(std::vector<AtomicProposition *> list) {
    if (list.size() <= 0) {
        return NULL;
    } else if (list.size() == 1) {
        return list.front();
    } else {
        size_t i = list.size();
        Proposition* result = new Disjunction(list.at(i-1), list.at(i-2));
        while (i - 2 > 0) {
            i--;
            result = new Disjunction(list.at(i), result);
        }
        std::cout << result->toString() << std::endl;
        return result;
    }
}

std::vector<AtomicProposition*> MainWindow::getUncertainVariables(int variable, std::vector<AtomicProposition *> variableList, std::vector<std::string> matrix) {
    std::vector<AtomicProposition*> list;

    for (size_t row = 0; row < mNumVariable; row++) {
        bool isSame = true;
        for (size_t column = 0; column < mNumVariable; column++) {
            if (matrix.at(row * mNumVariable + column).compare(matrix.at(variable * mNumVariable + column)) != 0) {
                isSame = false;
                break;
            }
        }
        if (isSame) {
            list.push_back(variableList.at(row));
        }
    }

    return list;
}

std::vector<AtomicAction*> MainWindow::generateActionList(std::vector<std::string> matrix) {
    std::vector<AtomicAction*> actionList;
    for (size_t i = 0; i < matrix.size(); i++) {
        if (matrix.at(i).compare("") == 0) {
            continue;
        }

        bool exist = false;
        for (size_t j = 0; j < actionList.size(); j++) {
            if (matrix[i].compare(actionList.at(j)->toString()) == 0) {
                exist = true;
                break;
            }
        }
        if (!exist) {
            actionList.push_back(new AtomicAction(matrix[i]));
        }
    }
    return actionList;
}

std::vector<std::string> MainWindow::generateMatrix(QTableWidget* widget) {
    std::vector<std::string> content;
    for (size_t i = 0; i < widget->rowCount(); i++) {
        for (size_t j = 0; j < widget->columnCount(); j++) {
            if (widget->item(i,j) == 0) {
                content.push_back("");
            } else {
                std::string str ("aa{");
                str += widget->item(i,j)->text().toUtf8().constData();
                str += "}";
                content.push_back(str);
            }
        }
    }
    return content;
}

void MainWindow::loadOxford()
{
    std::cout << "load file\n";
    std::ifstream ifs1 ( "resource/oxford_map.res" , std::ifstream::in );
    std::ifstream ifs2 ( "resource/oxford_path.res" , std::ifstream::in );

    std::cout << "file opened\n";

    std::vector<std::string> map;
    std::vector<std::string> path;

    char* content = (char*)malloc(sizeof(char)*256);
    while (!ifs1.eof()) {
        ifs1.getline(content, 256);
        std::string s (content);
        if (s.compare("@@@") == 0) {
            break;
        }
        map.push_back(s);
    }

    while (!ifs2.eof()) {
        ifs2.getline(content, 256);
        std::string s (content);
        if (s.compare("@@@") == 0) {
            break;
        }
        path.push_back(s);
    }

    std::cout << "file loaded:" << map.size() << "," << path.size() << std::endl;

    if (map.size() == path.size()) {
        double result = sqrt(map.size());
        //std::cout << "wtf286\n";
        if((int)result * (int)result == map.size()) {
            mNumVariable = (int)result;
            ui->mNumVariableSpin->setValue(mNumVariable);
            //std::cout << "wtf286\n";
            for (int i = 0; i < ui->mVariableTableWidget->rowCount(); i++) {
                ui->mVariableTableWidget->removeRow(i);
            }
            //std::cout << "wtf286\n";

            for (int i = 0; i < ui->mVariableTableWidget->columnCount(); i++) {
                ui->mVariableTableWidget->removeColumn(i);
            }
            //std::cout << "wtf286\n";

            for (int i = 0; i < mNumVariable; i++) {
                ui->mVariableTableWidget->insertRow(ui->mVariableTableWidget->rowCount());
                ui->mVariableTableWidget->insertColumn(ui->mVariableTableWidget->columnCount());
            }
            //std::cout << "wtf286\n";
            std::cout << "mNumVariable:" << mNumVariable << std::endl;

            for (int row = 0; row < mNumVariable; row++) {
                for (int column = 0; column < mNumVariable; column++) {
                    if (map.at(row * mNumVariable + column).compare("") == 0) {
                        continue;
                    }
                    QString qstr = QString::fromStdString(map.at(row * mNumVariable + column));
                    QTableWidgetItem *item = new QTableWidgetItem(qstr);
                    ui->mVariableTableWidget->setItem(row, column, item);
                }
            }
            //std::cout << "wtf286\n";


            //same operations for path table
            for (int i = 0; i < ui->mPathTableWidget->rowCount(); i++) {
                ui->mPathTableWidget->removeRow(i);
            }

            for (int i = 0; i < ui->mPathTableWidget->columnCount(); i++) {
                ui->mPathTableWidget->removeColumn(i);
            }

            for (int i = 0; i < mNumVariable; i++) {
                ui->mPathTableWidget->insertRow(ui->mPathTableWidget->rowCount());
                ui->mPathTableWidget->insertColumn(ui->mPathTableWidget->columnCount());
            }

            for (int row = 0; row < mNumVariable; row++) {
                for (int column = 0; column < mNumVariable; column++) {
                    if (path.at(row * mNumVariable + column).compare("") == 0) {
                        continue;
                    }
                    QString qstr = QString::fromStdString(path.at(row * mNumVariable + column));
                    QTableWidgetItem *item = new QTableWidgetItem(qstr);
                    ui->mPathTableWidget->setItem(row, column, item);
                }
            }
        }
    }

    ifs1.close();
    ifs2.close();
}

void MainWindow::on_actionOxford_Map_triggered()
{
    clearUI(true);
    loadOxford();
}

void MainWindow::on_mShowPDFButton_clicked()
{
    std::string head ("\\documentclass[5pt]{article}\n\\usepackage{amsmath}\n\\usepackage{amsfonts}\n\\usepackage{amssymb}\n\\usepackage{proof}\n\\begin{document}");
    std::string tail ("\\end{document}");
    std::ofstream output_file;
    output_file.open ("output/temp.tex", std::ios::trunc);
    output_file << head << std::endl;
    output_file << mResult << std::endl;
    output_file << tail << std::endl;
    output_file.close();
    system("pdflatex output/temp.tex");
    system("evince temp.pdf");
}

void MainWindow::on_rule_created(Rule * rule) {
    ruleitemwidget *myitem = new ruleitemwidget(this, rule);
    QListWidgetItem *item = new QListWidgetItem();
    item->setSizeHint(QSize(0,45));
    ui->mRuleListWidget->addItem(item);
    ui->mRuleListWidget->setItemWidget(item,myitem);
}

void MainWindow::on_rule_edited(Rule * rule) {
    QListWidgetItem *item = ui->mRuleListWidget->currentItem();
    ruleitemwidget *myitem = new ruleitemwidget(this, rule);
    ui->mRuleListWidget->setItemWidget(item,myitem);
}

void MainWindow::on_mAddRuleButton_clicked()
{
    RuleDialog *dialog = new RuleDialog(this, NULL);
    connect(dialog, SIGNAL(rule_created(Rule*)), this, SLOT(on_rule_created(Rule*)));
    dialog->exec();
}

void MainWindow::on_actionMatrix_triggered()
{
    ui->mStackedLeftWidget->setCurrentIndex(0);
    mIsMannual = false;
}

void MainWindow::on_actionMannual_triggered()
{
    ui->mStackedLeftWidget->setCurrentIndex(1);
    mIsMannual = true;
}

void MainWindow::on_mEditRuleButton_clicked()
{
    //    if (ui->mRuleListWidget->currentItem()  != 0) {
    //        ui->mRuleListWidget->
    //        Rule *rule =  ((ruleitemwidget*)ui->mRuleListWidget->currentItem())->getRule();
    //        std::cout << rule->toLatex() << std::endl;
    //        RuleDialog *dialog = new RuleDialog(this, rule);
    //        connect(dialog, SIGNAL(rule_edited(Rule*)), this, SLOT(on_rule_edited(Rule*)));
    //        dialog->exec();
    //    }
}

void MainWindow::on_mDeleteRuleButton_clicked()
{
    if (ui->mRuleListWidget->currentItem()  != 0) {
        ui->mRuleListWidget->takeItem(ui->mRuleListWidget->row(ui->mRuleListWidget->currentItem()));
    }
}

void MainWindow::on_actionCoin_Toss_triggered()
{
    clearUI(false);

    //Agents
    Agent *agentA = new Agent("A");
    Agent *agentB = new Agent("B");
    Agent *agentC = new Agent("C");

    //Proposition variables
    std::string strh("ap{H}");
    AtomicProposition *apH = new AtomicProposition(strh);
    std::string strt("ap{T}");
    AtomicProposition *apT = new AtomicProposition(strt);

    //Actions
    std::string strhannouce("aa{H!}");
    AtomicAction *hannounce = new AtomicAction(strhannouce);
    std::string strtannouce("aa{T!}");
    AtomicAction *tannounce = new AtomicAction(strtannouce);

    //Proposition apearance
    R_PrApp *rpappA1 = new R_PrApp(agentA, apH, new Disjunction(apH, apT));
    R_PrApp *rpappA2 = new R_PrApp(agentA, apT, new Disjunction(apH, apT));
    R_PrApp *rpappB1 = new R_PrApp(agentB, apH, new Disjunction(apH, apT));
    R_PrApp *rpappB2 = new R_PrApp(agentB, apT, new Disjunction(apH, apT));
    R_PrApp *rpappC1 = new R_PrApp(agentC, apH, apH);
    R_PrApp *rpappC2 = new R_PrApp(agentC, apT, apT);

    //Fact rules
    NavApp *napp11 = new NavApp(apH, hannounce, apH);
    NavApp *napp12 = new NavApp(apT, hannounce, apT);
    NavApp *napp13 = new NavApp(apH, tannounce, apH);
    NavApp *napp14 = new NavApp(apT, tannounce, apT);

    //action appearance
    R_App *rapp1 = new R_App(agentA, hannounce, hannounce);
    R_App *rapp2 = new R_App(agentA, tannounce, tannounce);
    R_App *rapp3 = new R_App(agentB, hannounce, hannounce);
    R_App *rapp4 = new R_App(agentB, tannounce, tannounce);
    R_App *rapp5 = new R_App(agentC, hannounce, hannounce);
    R_App *rapp6 = new R_App(agentC, tannounce, tannounce);

    //kernel rules
    R_Kernel *rker1 = new R_Kernel(hannounce, apT);
    R_Kernel *rker2 = new R_Kernel(tannounce, apH);

    std::vector<Rule*> list;
    list.push_back(rpappA1);
    list.push_back(rpappA2);
    list.push_back(rpappB1);
    list.push_back(rpappB2);
    list.push_back(rpappC1);
    list.push_back(rpappC2);


    list.push_back(rapp1);
    list.push_back(rapp2);
    list.push_back(rapp3);
    list.push_back(rapp4);
    list.push_back(rapp5);
    list.push_back(rapp6);

    list.push_back(napp11);
    list.push_back(napp12);
    list.push_back(napp13);
    list.push_back(napp14);

    list.push_back(rker1);
    list.push_back(rker2);



    for (size_t i = 0 ; i < list.size(); i++) {
        ruleitemwidget *myitem = new ruleitemwidget(this, list[i]);
        QListWidgetItem *item = new QListWidgetItem();
        item->setSizeHint(QSize(0,45));
        ui->mRuleListWidget->addItem(item);
        ui->mRuleListWidget->setItemWidget(item,myitem);
    }

    std::vector<Rule*> sys_rule = registerAllRules();
    for (size_t i = 0; i < list.size(); i++) {
        sys_rule.push_back(list[i]);
    }

    mRuleList = sys_rule;

    mIsMannual = true;
}

void MainWindow::clearUI(bool isMap) {
    if (isMap) {
        ui->mStackedLeftWidget->setCurrentIndex(0);
        ui->mVariableTableWidget->clear();
    } else {
        ui->mStackedLeftWidget->setCurrentIndex(1);
        ui->mRuleListWidget->clear();
    }

    ui->mInputSequentEdit->clear();
    ui->mOutputTextEdit->clear();
    mRuleList.clear();
}

void MainWindow::on_actionClassic_Map_2_triggered()
{
    clearUI(false);
    //Code robot navigation scenario
    //Agent A
    Agent *agent = new Agent("A");
    //Proposition variables
    std::string s_p1("ap{p_1}");
    std::string s_p2("ap{p_2}");
    std::string s_p3("ap{p_3}");
    std::string s_p4("ap{p_4}");
    std::string s_p5("ap{p_5}");
    AtomicProposition *p1 = new AtomicProposition(s_p1);
    AtomicProposition *p2 = new AtomicProposition(s_p2);
    AtomicProposition *p3 = new AtomicProposition(s_p3);
    AtomicProposition *p4 = new AtomicProposition(s_p4);
    AtomicProposition *p5 = new AtomicProposition(s_p5);

    Disjunction* dis_p1_p2 = new Disjunction(p1, p2);
    Disjunction* dis_p3_p4 = new Disjunction(p3, p4);
    //Proposition Appearance
    R_PrApp *rpapp1 = new R_PrApp(agent, p1, dis_p1_p2);
    R_PrApp *rpapp2 = new R_PrApp(agent, p2, dis_p1_p2);
    R_PrApp *rpapp3 = new R_PrApp(agent, p3, dis_p3_p4);
    R_PrApp *rpapp4 = new R_PrApp(agent, p4, dis_p3_p4);
    R_PrApp *rpapp5 = new R_PrApp(agent, p5, p5);

    //atomic actions and complements
    std::string s_a("aa{a}");
    std::string s_na("aa{\\bar{a}}");
    std::string s_b("aa{b}");
    std::string s_nb("aa{\\bar{b}}");
    std::string s_c("aa{c}");
    std::string s_nc("aa{\\bar{c}}");

    AtomicAction *a = new AtomicAction(s_a);
    AtomicAction *na = new AtomicAction(s_na);
    AtomicAction *b = new AtomicAction(s_b);
    AtomicAction *nb = new AtomicAction(s_nb);
    AtomicAction *c = new AtomicAction(s_c);
    AtomicAction *nc = new AtomicAction(s_nc);


    //std::cout << actionTable->findComplement(a)->toLatex() << std::endl;

    //Action Appearance
    R_App *rapp1 = new R_App(agent, a, a);
    R_App *rapp2 = new R_App(agent, b, b);
    R_App *rapp3 = new R_App(agent, c, c);
    R_App *rapp4 = new R_App(agent, na, na);
    R_App *rapp5 = new R_App(agent, nb, nb);
    R_App *rapp6 = new R_App(agent, nc, nc);

    //Nav Appearance
    std::string null("bt");
    Bottom *bottom = new Bottom(null);
    NavApp *napp11 = new NavApp(p1, a, p4);
    NavApp *napp12 = new NavApp(p1, b, p3);
    NavApp *napp13 = new NavApp(p1, c, bottom);
    NavApp *napp14 = new NavApp(p1, na, p2);
    NavApp *napp15 = new NavApp(p1, nb, bottom);
    NavApp *napp16 = new NavApp(p1, nc, bottom);

    NavApp *napp21 = new NavApp(p2, a, p1);
    NavApp *napp22 = new NavApp(p2, b, p3);
    NavApp *napp23 = new NavApp(p2, c, bottom);
    NavApp *napp24 = new NavApp(p2, na, bottom);
    NavApp *napp25 = new NavApp(p2, nb, bottom);
    NavApp *napp26 = new NavApp(p2, nc, bottom);

    NavApp *napp31 = new NavApp(p3, a, bottom);
    NavApp *napp32 = new NavApp(p3, b, bottom);
    NavApp *napp33 = new NavApp(p3, c, p5);
    NavApp *napp34 = new NavApp(p3, na, bottom);
    NavApp *napp35 = new NavApp(p3, nb, new Disjunction(p1, p2));
    NavApp *napp36 = new NavApp(p3, nc, bottom);

    NavApp *napp41 = new NavApp(p4, a, bottom);
    NavApp *napp42 = new NavApp(p4, b, bottom);
    NavApp *napp43 = new NavApp(p4, c, p5);
    NavApp *napp44 = new NavApp(p4, na, p1);
    NavApp *napp45 = new NavApp(p4, nb, bottom);
    NavApp *napp46 = new NavApp(p4, nc, bottom);

    NavApp *napp51 = new NavApp(p5, a, bottom);
    NavApp *napp52 = new NavApp(p5, b, bottom);
    NavApp *napp53 = new NavApp(p5, c, bottom);
    NavApp *napp54 = new NavApp(p5, na, bottom);
    NavApp *napp55 = new NavApp(p5, nb, bottom);
    NavApp *napp56 = new NavApp(p5, nc, new Disjunction(p3, p4));

    //Robot navigation learning rule
    //NavDyDist *navdydist = new NavDyDist(actionTable);

    //Robot real path
    NavPath *navpath = new NavPath();
    navpath->add(new NavStep(p1, a, p4));

    //Robot navigation forward nondeterminism rule
    NavFNDyDist *navfndydist = new NavFNDyDist(navpath);

    std::vector<Rule*> list;

    //Add navigation assumption rules
    list.push_back(navfndydist);

    list.push_back(rapp1);
    list.push_back(rapp2);
    list.push_back(rapp3);
    list.push_back(rapp4);
    list.push_back(rapp5);
    list.push_back(rapp6);

    list.push_back(rpapp1);
    list.push_back(rpapp2);
    list.push_back(rpapp3);
    list.push_back(rpapp4);
    list.push_back(rpapp5);

    list.push_back(napp11);
    list.push_back(napp12);
    list.push_back(napp13);
    list.push_back(napp14);
    list.push_back(napp15);
    list.push_back(napp16);

    list.push_back(napp21);
    list.push_back(napp22);
    list.push_back(napp23);
    list.push_back(napp24);
    list.push_back(napp25);
    list.push_back(napp26);

    list.push_back(napp31);
    list.push_back(napp32);
    list.push_back(napp33);
    list.push_back(napp34);
    list.push_back(napp35);
    list.push_back(napp36);

    list.push_back(napp41);
    list.push_back(napp42);
    list.push_back(napp43);
    list.push_back(napp44);
    list.push_back(napp45);
    list.push_back(napp46);

    list.push_back(napp51);
    list.push_back(napp52);
    list.push_back(napp53);
    list.push_back(napp54);
    list.push_back(napp55);
    list.push_back(napp56);


    for (size_t i = 0 ; i < list.size(); i++) {
        ruleitemwidget *myitem = new ruleitemwidget(this, list[i]);
        QListWidgetItem *item = new QListWidgetItem();
        item->setSizeHint(QSize(0,45));
        ui->mRuleListWidget->addItem(item);
        ui->mRuleListWidget->setItemWidget(item,myitem);
    }

    std::vector<Rule*> sys_rule = registerAllRules();
    for (size_t i = 0; i < sys_rule.size(); i++) {
        list.push_back(sys_rule[i]);
    }

    mRuleList = list;

    mIsMannual = true;

}

void MainWindow::on_actionBK_s_Map_2_triggered()
{
    clearUI(false);
    //Test for BK paper robot navigation.
    Agent *agent = new Agent("A");
    //Proposition variables
    std::string s_p1("ap{p_1}");
    std::string s_p2("ap{p_2}");
    std::string s_p3("ap{p_3}");
    std::string s_p4("ap{p_4}");
    std::string s_p5("ap{p_5}");
    std::string s_p6("ap{p_6}");
    std::string s_p7("ap{p_7}");
    std::string s_p8("ap{p_8}");
    std::string s_p9("ap{p_9}");
    std::string s_p10("ap{p_{10}}");
    std::string s_p11("ap{p_{11}}");
    std::string s_p12("ap{p_{12}}");
    std::string s_p13("ap{p_{13}}");
    std::string s_p14("ap{p_{14}}");
    std::string s_p15("ap{p_{15}}");
    std::string s_p16("ap{p_{16}}");
    std::string s_p17("ap{p_{17}}");
    std::string s_p18("ap{p_{18}}");
    std::string s_p19("ap{p_{19}}");
    std::string s_p20("ap{p_{20}}");
    AtomicProposition *p1 = new AtomicProposition(s_p1);
    AtomicProposition *p2 = new AtomicProposition(s_p2);
    AtomicProposition *p3 = new AtomicProposition(s_p3);
    AtomicProposition *p4 = new AtomicProposition(s_p4);
    AtomicProposition *p5 = new AtomicProposition(s_p5);
    AtomicProposition *p6 = new AtomicProposition(s_p6);
    AtomicProposition *p7 = new AtomicProposition(s_p7);
    AtomicProposition *p8 = new AtomicProposition(s_p8);
    AtomicProposition *p9 = new AtomicProposition(s_p9);
    AtomicProposition *p10 = new AtomicProposition(s_p10);
    AtomicProposition *p11 = new AtomicProposition(s_p11);
    AtomicProposition *p12 = new AtomicProposition(s_p12);
    AtomicProposition *p13 = new AtomicProposition(s_p13);
    AtomicProposition *p14 = new AtomicProposition(s_p14);
    AtomicProposition *p15 = new AtomicProposition(s_p15);
    AtomicProposition *p16 = new AtomicProposition(s_p16);
    AtomicProposition *p17 = new AtomicProposition(s_p17);
    AtomicProposition *p18 = new AtomicProposition(s_p18);
    AtomicProposition *p19 = new AtomicProposition(s_p19);
    AtomicProposition *p20 = new AtomicProposition(s_p20);

    //Proposition Appearance
    R_PrApp *rpapp1 = new R_PrApp(agent, p1, new Disjunction(p1, p17));
    R_PrApp *rpapp2 = new R_PrApp(agent, p2, p2);
    R_PrApp *rpapp3 = new R_PrApp(agent, p3, p3);
    R_PrApp *rpapp4 = new R_PrApp(agent, p4, new Disjunction(p4, p9));
    R_PrApp *rpapp5 = new R_PrApp(agent, p5,
                                  new Disjunction(p5, new Disjunction(p10, p18)));
    R_PrApp *rpapp6 = new R_PrApp(
                agent,
                p6,
                new Disjunction(p6,
                                new Disjunction(p11, new Disjunction(p16, p19))));
    R_PrApp *rpapp7 = new R_PrApp(agent, p7, p7);
    R_PrApp *rpapp8 = new R_PrApp(agent, p8, new Disjunction(p8, p15));
    R_PrApp *rpapp9 = new R_PrApp(agent, p9, new Disjunction(p4, p9));
    R_PrApp *rpapp10 = new R_PrApp(agent, p10,
                                   new Disjunction(p5, new Disjunction(p10, p18)));
    R_PrApp *rpapp11 = new R_PrApp(
                agent,
                p11,
                new Disjunction(p6,
                                new Disjunction(p11, new Disjunction(p16, p19))));
    R_PrApp *rpapp12 = new R_PrApp(agent, p12, p12);
    R_PrApp *rpapp13 = new R_PrApp(agent, p13, p13);
    R_PrApp *rpapp14 = new R_PrApp(agent, p14, p14);
    R_PrApp *rpapp15 = new R_PrApp(agent, p15, new Disjunction(p8, p15));
    R_PrApp *rpapp16 = new R_PrApp(
                agent,
                p16,
                new Disjunction(p6,
                                new Disjunction(p11, new Disjunction(p16, p19))));
    R_PrApp *rpapp17 = new R_PrApp(agent, p17, new Disjunction(p1, p17));
    R_PrApp *rpapp18 = new R_PrApp(agent, p18,
                                   new Disjunction(p5, new Disjunction(p10, p18)));
    R_PrApp *rpapp19 = new R_PrApp(
                agent,
                p19,
                new Disjunction(p6,
                                new Disjunction(p11, new Disjunction(p16, p19))));
    R_PrApp *rpapp20 = new R_PrApp(agent, p20, p20);

    //atomic actions and complements
    std::string s_n("aa{n}");
    std::string s_s("aa{s}");
    std::string s_w("aa{w}");
    std::string s_e("aa{e}");
    std::string s_nw("aa{nw}");
    std::string s_se("aa{se}");

    AtomicAction *n = new AtomicAction(s_n);
    AtomicAction *s = new AtomicAction(s_s);
    AtomicAction *w = new AtomicAction(s_w);
    AtomicAction *e = new AtomicAction(s_e);
    AtomicAction *nw = new AtomicAction(s_nw);
    AtomicAction *se = new AtomicAction(s_se);


    //std::cout << actionTable->findComplement(b)->toLatex() << std::endl;

    //Action Appearance
    R_App *rapp1 = new R_App(agent, n, n);
    R_App *rapp2 = new R_App(agent, s, s);
    R_App *rapp3 = new R_App(agent, w, w);
    R_App *rapp4 = new R_App(agent, e, e);
    R_App *rapp5 = new R_App(agent, nw, nw);
    R_App *rapp6 = new R_App(agent, se, se);

    //Nav Appearance
    std::string null("bt");
    Bottom *bottom = new Bottom(null);
    NavApp *napp11 = new NavApp(p1, n, p7);
    NavApp *napp12 = new NavApp(p1, s, bottom);
    NavApp *napp13 = new NavApp(p1, w, p2);
    NavApp *napp14 = new NavApp(p1, e, p8);
    NavApp *napp15 = new NavApp(p1, nw, bottom);
    NavApp *napp16 = new NavApp(p1, se, bottom);
    NavApp *napp21 = new NavApp(p2, n, bottom);
    NavApp *napp22 = new NavApp(p2, s, bottom);
    NavApp *napp23 = new NavApp(p2, w, bottom);
    NavApp *napp24 = new NavApp(p2, e, p1);
    NavApp *napp25 = new NavApp(p2, nw, p3);
    NavApp *napp26 = new NavApp(p2, se, bottom);
    NavApp *napp31 = new NavApp(p3, n, p4);
    NavApp *napp32 = new NavApp(p3, s, bottom);
    NavApp *napp33 = new NavApp(p3, w, bottom);
    NavApp *napp34 = new NavApp(p3, e, bottom);
    NavApp *napp35 = new NavApp(p3, nw, bottom);
    NavApp *napp36 = new NavApp(p3, se, p2);
    NavApp *napp41 = new NavApp(p4, n, p5);
    NavApp *napp42 = new NavApp(p4, s, p3);
    NavApp *napp43 = new NavApp(p4, w, bottom);
    NavApp *napp44 = new NavApp(p4, e, p7);
    NavApp *napp45 = new NavApp(p4, nw, bottom);
    NavApp *napp46 = new NavApp(p4, se, bottom);
    NavApp *napp51 = new NavApp(p5, n, bottom);
    NavApp *napp52 = new NavApp(p5, s, p4);
    NavApp *napp53 = new NavApp(p5, w, bottom);
    NavApp *napp54 = new NavApp(p5, e, p6);
    NavApp *napp55 = new NavApp(p5, nw, bottom);
    NavApp *napp56 = new NavApp(p5, se, bottom);
    NavApp *napp61 = new NavApp(p6, n, bottom);
    NavApp *napp62 = new NavApp(p6, s, p7);
    NavApp *napp63 = new NavApp(p6, w, p5);
    NavApp *napp64 = new NavApp(p6, e, bottom);
    NavApp *napp65 = new NavApp(p6, nw, bottom);
    NavApp *napp66 = new NavApp(p6, se, bottom);
    NavApp *napp71 = new NavApp(p7, n, p6);
    NavApp *napp72 = new NavApp(p7, s, p1);
    NavApp *napp73 = new NavApp(p7, w, p4);
    NavApp *napp74 = new NavApp(p7, e, bottom);
    NavApp *napp75 = new NavApp(p7, nw, bottom);
    NavApp *napp76 = new NavApp(p7, se, bottom);
    NavApp *napp81 = new NavApp(p8, n, p9);
    NavApp *napp82 = new NavApp(p8, s, bottom);
    NavApp *napp83 = new NavApp(p8, w, p1);
    NavApp *napp84 = new NavApp(p8, e, bottom);
    NavApp *napp85 = new NavApp(p8, nw, bottom);
    NavApp *napp86 = new NavApp(p8, se, bottom);
    NavApp *napp91 = new NavApp(p9, n, p10);
    NavApp *napp92 = new NavApp(p9, s, p9);
    NavApp *napp93 = new NavApp(p9, w, bottom);
    NavApp *napp94 = new NavApp(p9, e, p12);
    NavApp *napp95 = new NavApp(p9, nw, bottom);
    NavApp *napp96 = new NavApp(p9, se, bottom);
    NavApp *napp101 = new NavApp(p10, n, bottom);
    NavApp *napp102 = new NavApp(p10, s, p9);
    NavApp *napp103 = new NavApp(p10, w, bottom);
    NavApp *napp104 = new NavApp(p10, e, p11);
    NavApp *napp105 = new NavApp(p10, nw, bottom);
    NavApp *napp106 = new NavApp(p10, se, bottom);
    NavApp *napp111 = new NavApp(p11, n, bottom);
    NavApp *napp112 = new NavApp(p11, s, p12);
    NavApp *napp113 = new NavApp(p11, w, p10);
    NavApp *napp114 = new NavApp(p11, e, bottom);
    NavApp *napp115 = new NavApp(p11, nw, bottom);
    NavApp *napp116 = new NavApp(p11, se, bottom);
    NavApp *napp121 = new NavApp(p12, n, p11);
    NavApp *napp122 = new NavApp(p12, s, p13);
    NavApp *napp123 = new NavApp(p12, w, p9);
    NavApp *napp124 = new NavApp(p12, e, p17);
    NavApp *napp125 = new NavApp(p12, nw, bottom);
    NavApp *napp126 = new NavApp(p12, se, bottom);
    NavApp *napp131 = new NavApp(p13, n, p12);
    NavApp *napp132 = new NavApp(p13, s, bottom);
    NavApp *napp133 = new NavApp(p13, w, bottom);
    NavApp *napp134 = new NavApp(p13, e, p14);
    NavApp *napp135 = new NavApp(p13, nw, bottom);
    NavApp *napp136 = new NavApp(p13, se, bottom);
    NavApp *napp141 = new NavApp(p14, n, bottom);
    NavApp *napp142 = new NavApp(p14, s, bottom);
    NavApp *napp143 = new NavApp(p14, w, p13);
    NavApp *napp144 = new NavApp(p14, e, p15);
    NavApp *napp145 = new NavApp(p14, nw, bottom);
    NavApp *napp146 = new NavApp(p14, se, bottom);
    NavApp *napp151 = new NavApp(p15, n, p16);
    NavApp *napp152 = new NavApp(p15, s, bottom);
    NavApp *napp153 = new NavApp(p15, w, p14);
    NavApp *napp154 = new NavApp(p15, e, bottom);
    NavApp *napp155 = new NavApp(p15, nw, bottom);
    NavApp *napp156 = new NavApp(p15, se, bottom);
    NavApp *napp161 = new NavApp(p16, n, bottom);
    NavApp *napp162 = new NavApp(p16, s, p15);
    NavApp *napp163 = new NavApp(p16, w, p17);
    NavApp *napp164 = new NavApp(p16, e, bottom);
    NavApp *napp165 = new NavApp(p16, nw, bottom);
    NavApp *napp166 = new NavApp(p16, se, bottom);
    NavApp *napp171 = new NavApp(p17, n, p18);
    NavApp *napp172 = new NavApp(p17, s, bottom);
    NavApp *napp173 = new NavApp(p17, w, p12);
    NavApp *napp174 = new NavApp(p17, e, p16);
    NavApp *napp175 = new NavApp(p17, nw, bottom);
    NavApp *napp176 = new NavApp(p17, se, bottom);
    NavApp *napp181 = new NavApp(p18, n, bottom);
    NavApp *napp182 = new NavApp(p18, s, p17);
    NavApp *napp183 = new NavApp(p18, w, bottom);
    NavApp *napp184 = new NavApp(p18, e, p19);
    NavApp *napp185 = new NavApp(p18, nw, bottom);
    NavApp *napp186 = new NavApp(p18, se, bottom);
    NavApp *napp191 = new NavApp(p19, n, bottom);
    NavApp *napp192 = new NavApp(p19, s, p20);
    NavApp *napp193 = new NavApp(p19, w, p18);
    NavApp *napp194 = new NavApp(p19, e, bottom);
    NavApp *napp195 = new NavApp(p19, nw, bottom);
    NavApp *napp196 = new NavApp(p19, se, bottom);
    NavApp *napp201 = new NavApp(p20, n, p19);
    NavApp *napp202 = new NavApp(p20, s, bottom);
    NavApp *napp203 = new NavApp(p20, w, bottom);
    NavApp *napp204 = new NavApp(p20, e, bottom);
    NavApp *napp205 = new NavApp(p20, nw, bottom);
    NavApp *napp206 = new NavApp(p20, se, bottom);

    //Robot navigation learning rule
    //NavDyDist *navdydist = new NavDyDist(actionTable);

    //Robot real path
    NavPath *navpath = new NavPath();
    navpath->add(new NavStep(p2, nw, p3));
    navpath->add(new NavStep(p3, s, p4));
    navpath->add(new NavStep(p4, e, p7));
    navpath->add(new NavStep(p7, s, p1));

    //Robot navigation forward nondeterminism rule
    NavFNDyDist *navfndydist = new NavFNDyDist(navpath);

    std::vector<Rule*> list;

    //Add navigation assumption rules
    //list.push_back(navdydist);
    //list.push_back(navfndydist);

    list.push_back(rapp1);
    list.push_back(rapp2);
    list.push_back(rapp3);
    list.push_back(rapp4);
    list.push_back(rapp5);
    list.push_back(rapp6);

    list.push_back(rpapp1);
    list.push_back(rpapp2);
    list.push_back(rpapp3);
    list.push_back(rpapp4);
    list.push_back(rpapp5);
    list.push_back(rpapp6);
    list.push_back(rpapp7);
    list.push_back(rpapp8);
    list.push_back(rpapp9);
    list.push_back(rpapp10);
    list.push_back(rpapp11);
    list.push_back(rpapp12);
    list.push_back(rpapp13);
    list.push_back(rpapp14);
    list.push_back(rpapp15);
    list.push_back(rpapp16);
    list.push_back(rpapp17);
    list.push_back(rpapp18);
    list.push_back(rpapp19);
    list.push_back(rpapp20);

    list.push_back(napp11);
    list.push_back(napp12);
    list.push_back(napp13);
    list.push_back(napp14);
    list.push_back(napp15);
    list.push_back(napp16);
    list.push_back(napp21);
    list.push_back(napp22);
    list.push_back(napp23);
    list.push_back(napp24);
    list.push_back(napp25);
    list.push_back(napp26);
    list.push_back(napp31);
    list.push_back(napp32);
    list.push_back(napp33);
    list.push_back(napp34);
    list.push_back(napp35);
    list.push_back(napp36);
    list.push_back(napp41);
    list.push_back(napp42);
    list.push_back(napp43);
    list.push_back(napp44);
    list.push_back(napp45);
    list.push_back(napp46);
    list.push_back(napp51);
    list.push_back(napp52);
    list.push_back(napp53);
    list.push_back(napp54);
    list.push_back(napp55);
    list.push_back(napp56);
    list.push_back(napp61);
    list.push_back(napp62);
    list.push_back(napp63);
    list.push_back(napp64);
    list.push_back(napp65);
    list.push_back(napp66);
    list.push_back(napp71);
    list.push_back(napp72);
    list.push_back(napp73);
    list.push_back(napp74);
    list.push_back(napp75);
    list.push_back(napp76);
    list.push_back(napp81);
    list.push_back(napp82);
    list.push_back(napp83);
    list.push_back(napp84);
    list.push_back(napp85);
    list.push_back(napp86);
    list.push_back(napp91);
    list.push_back(napp92);
    list.push_back(napp93);
    list.push_back(napp94);
    list.push_back(napp95);
    list.push_back(napp96);
    list.push_back(napp101);
    list.push_back(napp102);
    list.push_back(napp103);
    list.push_back(napp104);
    list.push_back(napp105);
    list.push_back(napp106);
    list.push_back(napp111);
    list.push_back(napp112);
    list.push_back(napp113);
    list.push_back(napp114);
    list.push_back(napp115);
    list.push_back(napp116);
    list.push_back(napp121);
    list.push_back(napp122);
    list.push_back(napp123);
    list.push_back(napp124);
    list.push_back(napp125);
    list.push_back(napp126);
    list.push_back(napp131);
    list.push_back(napp132);
    list.push_back(napp133);
    list.push_back(napp134);
    list.push_back(napp135);
    list.push_back(napp136);
    list.push_back(napp141);
    list.push_back(napp142);
    list.push_back(napp143);
    list.push_back(napp144);
    list.push_back(napp145);
    list.push_back(napp146);
    list.push_back(napp151);
    list.push_back(napp152);
    list.push_back(napp153);
    list.push_back(napp154);
    list.push_back(napp155);
    list.push_back(napp156);
    list.push_back(napp161);
    list.push_back(napp162);
    list.push_back(napp163);
    list.push_back(napp164);
    list.push_back(napp165);
    list.push_back(napp166);
    list.push_back(napp171);
    list.push_back(napp172);
    list.push_back(napp173);
    list.push_back(napp174);
    list.push_back(napp175);
    list.push_back(napp176);
    list.push_back(napp181);
    list.push_back(napp182);
    list.push_back(napp183);
    list.push_back(napp184);
    list.push_back(napp185);
    list.push_back(napp186);
    list.push_back(napp191);
    list.push_back(napp192);
    list.push_back(napp193);
    list.push_back(napp194);
    list.push_back(napp195);
    list.push_back(napp196);
    list.push_back(napp201);
    list.push_back(napp202);
    list.push_back(napp203);
    list.push_back(napp204);
    list.push_back(napp205);
    list.push_back(napp206);

    for (size_t i = 0 ; i < list.size(); i++) {
        ruleitemwidget *myitem = new ruleitemwidget(this, list[i]);
        QListWidgetItem *item = new QListWidgetItem();
        item->setSizeHint(QSize(0,45));
        ui->mRuleListWidget->addItem(item);
        ui->mRuleListWidget->setItemWidget(item,myitem);
    }

    std::vector<Rule*> sys_rule = registerAllRules();
    for (size_t i = 0; i < sys_rule.size(); i++) {
        list.push_back(sys_rule[i]);
    }

    mRuleList = list;

    mIsMannual = true;

}

void MainWindow::on_actionStaircase_triggered()
{
    clearUI(false);
    //Test for staircase navigation. For simplicity, only 10 stairs are coded.
    Agent *agent = new Agent("A");
    //Proposition variables
    std::string s_p1("ap{p_1}");
    std::string s_p2("ap{p_2}");
    std::string s_p3("ap{p_3}");
    std::string s_p4("ap{p_4}");
    std::string s_p5("ap{p_5}");
    std::string s_p6("ap{p_6}");
    std::string s_p7("ap{p_7}");
    std::string s_p8("ap{p_8}");
    std::string s_p9("ap{p_9}");
    std::string s_p10("ap{p_{10}}");
    AtomicProposition *p1 = new AtomicProposition(s_p1);
    AtomicProposition *p2 = new AtomicProposition(s_p2);
    AtomicProposition *p3 = new AtomicProposition(s_p3);
    AtomicProposition *p4 = new AtomicProposition(s_p4);
    AtomicProposition *p5 = new AtomicProposition(s_p5);
    AtomicProposition *p6 = new AtomicProposition(s_p6);
    AtomicProposition *p7 = new AtomicProposition(s_p7);
    AtomicProposition *p8 = new AtomicProposition(s_p8);
    AtomicProposition *p9 = new AtomicProposition(s_p9);
    AtomicProposition *p10 = new AtomicProposition(s_p10);

    std::string middle_stairs(
                "dj{ap{p_2}}{dj{ap{p_3}}{dj{ap{p_4}}{dj{ap{p_5}}{dj{ap{p_6}}{dj{ap{p_7}}{dj{ap{p_8}}{ap{p_9}}}}}}}}");
    Disjunction* middle_uncertainty = (Disjunction*) createProposition(
                middle_stairs);
    //Proposition Appearance
    R_PrApp *rpapp1 = new R_PrApp(agent, p1, p1);
    R_PrApp *rpapp2 = new R_PrApp(agent, p2, middle_uncertainty);
    R_PrApp *rpapp3 = new R_PrApp(agent, p3, middle_uncertainty);
    R_PrApp *rpapp4 = new R_PrApp(agent, p4, middle_uncertainty);
    R_PrApp *rpapp5 = new R_PrApp(agent, p5, middle_uncertainty);
    R_PrApp *rpapp6 = new R_PrApp(agent, p6, middle_uncertainty);
    R_PrApp *rpapp7 = new R_PrApp(agent, p7, middle_uncertainty);
    R_PrApp *rpapp8 = new R_PrApp(agent, p8, middle_uncertainty);
    R_PrApp *rpapp9 = new R_PrApp(agent, p9, middle_uncertainty);
    R_PrApp *rpapp10 = new R_PrApp(agent, p10, p10);

    //atomic actions and complements
    std::string s_a("aa{up}");
    std::string s_b("aa{down}");

    AtomicAction *a = new AtomicAction(s_a);
    AtomicAction *b = new AtomicAction(s_b);

    //std::cout << actionTable->findComplement(b)->toLatex() << std::endl;

    //Action Appearance
    R_App *rapp1 = new R_App(agent, a, a);
    R_App *rapp2 = new R_App(agent, b, b);

    //Nav Appearance
    std::string null("bt");
    Bottom *bottom = new Bottom(null);
    NavApp *napp11 = new NavApp(p1, a, p2);
    NavApp *napp12 = new NavApp(p1, b, bottom);
    NavApp *napp21 = new NavApp(p2, a, p3);
    NavApp *napp22 = new NavApp(p2, b, p1);
    NavApp *napp31 = new NavApp(p3, a, p4);
    NavApp *napp32 = new NavApp(p3, b, p2);
    NavApp *napp41 = new NavApp(p4, a, p5);
    NavApp *napp42 = new NavApp(p4, b, p3);
    NavApp *napp51 = new NavApp(p5, a, p6);
    NavApp *napp52 = new NavApp(p5, b, p4);
    NavApp *napp61 = new NavApp(p6, a, p7);
    NavApp *napp62 = new NavApp(p6, b, p5);
    NavApp *napp71 = new NavApp(p7, a, p8);
    NavApp *napp72 = new NavApp(p7, b, p6);
    NavApp *napp81 = new NavApp(p8, a, p9);
    NavApp *napp82 = new NavApp(p8, b, p7);
    NavApp *napp91 = new NavApp(p9, a, p10);
    NavApp *napp92 = new NavApp(p9, b, p8);
    NavApp *napp101 = new NavApp(p10, a, bottom);
    NavApp *napp102 = new NavApp(p10, b, p9);

    //Robot navigation learning rule
    //NavDyDist *navdydist = new NavDyDist(actionTable);

    //Robot real path
    NavPath *navpath = new NavPath();
    navpath->add(new NavStep(p2, a, p3));
    navpath->add(new NavStep(p3, b, p2));
    navpath->add(new NavStep(p2, b, p1));
    navpath->add(new NavStep(p1, a, p2));

    //Robot navigation forward nondeterminism rule
    NavFNDyDist *navfndydist = new NavFNDyDist(navpath);

    std::vector<Rule*> list;

    //Add navigation assumption rules
    //list.push_back(navdydist);
    //list.push_back(navfndydist);

    list.push_back(rapp1);
    list.push_back(rapp2);

    list.push_back(rpapp1);
    list.push_back(rpapp2);
    list.push_back(rpapp3);
    list.push_back(rpapp4);
    list.push_back(rpapp5);
    list.push_back(rpapp6);
    list.push_back(rpapp7);
    list.push_back(rpapp8);
    list.push_back(rpapp9);
    list.push_back(rpapp10);

    list.push_back(napp11);
    list.push_back(napp12);
    list.push_back(napp21);
    list.push_back(napp22);
    list.push_back(napp31);
    list.push_back(napp32);

    list.push_back(napp41);
    list.push_back(napp42);
    list.push_back(napp51);
    list.push_back(napp52);
    list.push_back(napp61);
    list.push_back(napp62);

    list.push_back(napp71);
    list.push_back(napp72);
    list.push_back(napp81);
    list.push_back(napp82);
    list.push_back(napp91);
    list.push_back(napp92);

    list.push_back(napp101);
    list.push_back(napp102);

    for (size_t i = 0 ; i < list.size(); i++) {
        ruleitemwidget *myitem = new ruleitemwidget(this, list[i]);
        QListWidgetItem *item = new QListWidgetItem();
        item->setSizeHint(QSize(0,45));
        ui->mRuleListWidget->addItem(item);
        ui->mRuleListWidget->setItemWidget(item,myitem);
    }

    std::vector<Rule*> sys_rule = registerAllRules();
    for (size_t i = 0; i < sys_rule.size(); i++) {
        list.push_back(sys_rule[i]);
    }

    mRuleList = list;

    mIsMannual = true;
}


void MainWindow::on_actionMuddyChildren_triggered()
{
    clearUI(false);
    //Agents
    Agent *agent1 = new Agent("1");
    Agent *agent2 = new Agent("2");
    Agent *agent3 = new Agent("3");

    //Propositions
    std::string strc1("ap{C1}");
    AtomicProposition *c1 = new AtomicProposition(strc1);
    std::string strd1("ap{D1}");
    AtomicProposition *d1 = new AtomicProposition(strd1);
    std::string strc2("ap{C2}");
    AtomicProposition *c2 = new AtomicProposition(strc2);
    std::string strd2("ap{D2}");
    AtomicProposition *d2 = new AtomicProposition(strd2);
    std::string strc3("ap{C3}");
    AtomicProposition *c3 = new AtomicProposition(strc3);
    std::string strd3("ap{D3}");
    AtomicProposition *d3 = new AtomicProposition(strd3);

    //Proposition apearance
    R_PrApp *rpapp11 = new R_PrApp(agent1, c1, new Disjunction(c1, d1));
    R_PrApp *rpapp12 = new R_PrApp(agent1, d1, new Disjunction(c1, d1));
    R_PrApp *rpapp13 = new R_PrApp(agent1, c2, c2);
    R_PrApp *rpapp14 = new R_PrApp(agent1, d2, d2);
    R_PrApp *rpapp15 = new R_PrApp(agent1, c3, c3);
    R_PrApp *rpapp16 = new R_PrApp(agent1, d3, d3);

    R_PrApp *rpapp21 = new R_PrApp(agent2, c2, new Disjunction(c2, d2));
    R_PrApp *rpapp22 = new R_PrApp(agent2, d2, new Disjunction(c2, d2));
    R_PrApp *rpapp23 = new R_PrApp(agent2, c1, c1);
    R_PrApp *rpapp24 = new R_PrApp(agent2, d1, d1);
    R_PrApp *rpapp25 = new R_PrApp(agent2, c3, c3);
    R_PrApp *rpapp26 = new R_PrApp(agent2, d3, d3);

    R_PrApp *rpapp31 = new R_PrApp(agent3, c3, new Disjunction(c3, d3));
    R_PrApp *rpapp32 = new R_PrApp(agent3, d3, new Disjunction(c3, d3));
    R_PrApp *rpapp33 = new R_PrApp(agent3, c2, c2);
    R_PrApp *rpapp34 = new R_PrApp(agent3, d2, d2);
    R_PrApp *rpapp35 = new R_PrApp(agent3, c1, c1);
    R_PrApp *rpapp36 = new R_PrApp(agent3, d1, d1);

    //Actions
    std::string strdadannouce("aa{d}");
    AtomicAction *dadannounce = new AtomicAction(strdadannouce);
    std::string strchildannouce("aa{d'}");
    AtomicAction *childannounce = new AtomicAction(strchildannouce);

    //Fact rules
    NavApp *napp11 = new NavApp(c1, dadannounce, c1);
    NavApp *napp12 = new NavApp(c2, dadannounce, c2);
    NavApp *napp13 = new NavApp(c3, dadannounce, c3);
    NavApp *napp14 = new NavApp(d1, dadannounce, d1);
    NavApp *napp15 = new NavApp(d2, dadannounce, d2);
    NavApp *napp16 = new NavApp(d3, dadannounce, d3);
    NavApp *napp21 = new NavApp(c1, childannounce, c1);
    NavApp *napp22 = new NavApp(c2, childannounce, c2);
    NavApp *napp23 = new NavApp(c3, childannounce, c3);
    NavApp *napp24 = new NavApp(d1, childannounce, d1);
    NavApp *napp25 = new NavApp(d2, childannounce, d2);
    NavApp *napp26 = new NavApp(d3, childannounce, d3);

    //action appearance
    R_App *rapp1 = new R_App(agent1, dadannounce, dadannounce);
    R_App *rapp2 = new R_App(agent2, dadannounce, dadannounce);
    R_App *rapp3 = new R_App(agent3, dadannounce, dadannounce);
    R_App *rapp4 = new R_App(agent1, childannounce, childannounce);
    R_App *rapp5 = new R_App(agent2, childannounce, childannounce);
    R_App *rapp6 = new R_App(agent3, childannounce, childannounce);

    //kernel rules
    std::string str("dj{sq{2}{ap{D2}}}{dj{sq{1}{ap{D1}}}{sq{3}{ap{D3}}}}");
    Proposition *disjunction = createProposition(str);
    R_Kernel *rker1 = new R_Kernel(dadannounce,
                                   new Conjunction(c1, new Conjunction(c2, c3)));
    R_Kernel *rker2 = new R_Kernel(childannounce, disjunction);

    std::vector<Rule*> list;

    list.push_back(rpapp11);
    list.push_back(rpapp12);
    list.push_back(rpapp13);
    list.push_back(rpapp14);
    list.push_back(rpapp15);
    list.push_back(rpapp16);
    list.push_back(rpapp21);
    list.push_back(rpapp22);
    list.push_back(rpapp23);
    list.push_back(rpapp24);
    list.push_back(rpapp25);
    list.push_back(rpapp26);
    list.push_back(rpapp31);
    list.push_back(rpapp32);
    list.push_back(rpapp33);
    list.push_back(rpapp34);
    list.push_back(rpapp35);
    list.push_back(rpapp36);

    list.push_back(rapp1);
    list.push_back(rapp2);
    list.push_back(rapp3);
    list.push_back(rapp4);
    list.push_back(rapp5);
    list.push_back(rapp6);

    list.push_back(rker1);
    list.push_back(rker2);

    list.push_back(napp11);
    list.push_back(napp12);
    list.push_back(napp13);
    list.push_back(napp14);
    list.push_back(napp15);
    list.push_back(napp16);
    list.push_back(napp21);
    list.push_back(napp22);
    list.push_back(napp23);
    list.push_back(napp24);
    list.push_back(napp25);
    list.push_back(napp26);

    for (size_t i = 0 ; i < list.size(); i++) {
        ruleitemwidget *myitem = new ruleitemwidget(this, list[i]);
        QListWidgetItem *item = new QListWidgetItem();
        item->setSizeHint(QSize(0,45));
        ui->mRuleListWidget->addItem(item);
        ui->mRuleListWidget->setItemWidget(item,myitem);
    }

    std::vector<Rule*> sys_rule = registerAllRules();
    for (size_t i = 0; i < sys_rule.size(); i++) {
        list.push_back(sys_rule[i]);
    }

    mRuleList = list;

    mIsMannual = true;
}
